package model.cnf;
import java.util.List;


/**
 * Represent some statistic on a CNF.
 * @author stephane
 *
 */
public class Stat{

	public static final int UNKNOW_VALUE = -1;
	
	private int numVar = UNKNOW_VALUE;
	private int numLiteral = UNKNOW_VALUE;
	private int numClause = UNKNOW_VALUE;
	private int numUnitClause = UNKNOW_VALUE;
	private int numBinaryClause = UNKNOW_VALUE;

	private double averageNumOfLiteralPerClause = -1;

	public Stat(MemoryCNF cnf_input) throws Exception{
		computeStat(cnf_input);
	}

	public Stat(FileCNF cnf_input) throws Exception{
		computeStat(cnf_input);
	}
	
	public Stat(){
		
	}

	/**
	 * optimized for MemoryCNF
	 * @param cnf the cnf
	 * @throws Exception
	 */
	public void computeStat(MemoryCNF cnf) throws Exception{
		List<Clause> my_clause = cnf.getClauses();
		numLiteral = numUnitClause = numBinaryClause = 0;
		
		numClause=my_clause.size();
		for(int i=0;i<numClause;i++){
			Clause cl=my_clause.get(i);
			if(cl.isUnit()) numUnitClause++;
			if(cl.isBinary()) numBinaryClause++;
			numLiteral+=cl.size();
		}
		averageNumOfLiteralPerClause=(double) numLiteral/numClause ;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause*1000.0) / 1000.0;
		numVar=cnf.getNumVar();
	}

	/**
	 * Optimized for FileCNF
	 * @param cnf the cnf
	 * @throws Exception 
	 */
	public void computeStat(FileCNF cnf) throws Exception{
		numLiteral = numUnitClause = numBinaryClause = 0;
		
		cnf.check();
		numClause = cnf.getDeclaredNumClause();
		numVar = cnf.getDeclaredNumVar();
		
		for(int i=0 ; i < numClause ; i++){
			Clause cl = cnf.getNextClause();
			if(cl.isUnit()) numUnitClause++;
			if(cl.isBinary()) numBinaryClause++;
			numLiteral+=cl.size();
		}
		
		averageNumOfLiteralPerClause=(double) numLiteral/numClause ;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause*1000.0) / 1000.0;
		
	}



	public String toString(){
		return "#Variables : " + numVar
		+ "\n#Clauses : " + numClause
		+ "\n#Literals : " + numLiteral 
		+ "\n#Unit clauses : " + numUnitClause
		+ "\n#Binary clauses : " + numBinaryClause
		+ "\nAverage lit/clause : " + averageNumOfLiteralPerClause;	
	}

	public int getNumVar(){return numVar;}
	public int getNumLiteral(){ return numLiteral; }
	public int getNumClause(){ return numClause;  }
	public int getNumUnitClause(){ return numUnitClause; }
	public int getNumBinaryClause(){ return numBinaryClause; }
	

	public void setNumVar(int numVar) {
		if(numVar == UNKNOW_VALUE || numVar >=0)
			this.numVar = numVar;
	}


	public void setNumLiteral(int numLiteral) {
		if(numLiteral == UNKNOW_VALUE || numLiteral >=0)
		{
			this.numLiteral = numLiteral;
			if(numLiteral != UNKNOW_VALUE && numClause != UNKNOW_VALUE)
			{
				averageNumOfLiteralPerClause=(double) numLiteral/numClause ;
				averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause*1000.0) / 1000.0;
			}
		}
	}


	public void setNumClause(int numClause) {
		if(numClause == UNKNOW_VALUE || numClause >=0)
		{
			this.numClause = numClause;
			if(numLiteral != UNKNOW_VALUE && numClause != UNKNOW_VALUE)
			{
				averageNumOfLiteralPerClause=(double) numLiteral/numClause ;
				averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause*1000.0) / 1000.0;
			}
		}
		
	}


	public void setNumUnitClause(int numUnitClause) {
		this.numUnitClause = numUnitClause;
	}


	public void setNumBinaryClause(int numBinaryClause) {
		this.numBinaryClause = numBinaryClause;
	}
	
	public void addClause(Clause clause, int nbVar){
		numClause++ ;
		if(clause.isUnit()) numUnitClause++;
		if(clause.isBinary()) numBinaryClause++;
		numLiteral += clause.size();
		
		averageNumOfLiteralPerClause = (double) numLiteral/numClause ;
		averageNumOfLiteralPerClause = Math.round(averageNumOfLiteralPerClause*1000.0) / 1000.0;
		numVar += nbVar;
	}
	

	public boolean equals(Object o){
		if (!(o instanceof Stat)) return false;
		Stat s=(Stat) o;
		if(numVar!=s.getNumVar()) return false;
		if(numLiteral!=s.getNumLiteral()) return false;
		if(numClause!=s.getNumClause()) return false;
		if(numUnitClause!=s.getNumUnitClause()) return false;
		if(numBinaryClause!=s.getNumBinaryClause()) return false;
		return true;
	}
}